COMMENT ⊗   VALID 00001 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 ENDMK
C⊗;
∂03-Apr-79  1041	FWH  
PASCAL 

%    ST in terms:	TRUE if term is a variable.
     SL in termlists:	TRUE if list is NOT empty ("NIL").
     SS in substitutions:  TRUE if sub is identity (empty subst.).
     FL in substitutions:  TRUE if object is not a unifier (used for
	returning failure).
%

TYPE VAR = INTEGER;	% dummy type definition %
TYPE FCN = INTEGER;	% dummy type definition %
TYPE TERM = RECORD ST:BOOLEAN; VT:VAR; FNLT:FCN; ARGS: ↑TERMLIST END;
TYPE TERMLIST = RECORD SL:BOOLEAN; HD: TERM; TL: ↑TERMLIST END;
TYPE SINGLESUB = RECORD VR:VAR;TM:TERM END;
TYPE SUB = RECORD FL:BOOLEAN; SS:BOOLEAN; CAR:SINGLESUB; CDR: ↑SUB END;

VAR S,ZEROSUB: SUB;
    X,Y: TERMLIST;

PROCEDURE TSUBSTP(X:TERM; S:SUB; VAR Y:TERM);
	EXIT Y=TSUBST(X,S);
	EXTERNAL;

FUNCTION PAIR(X:TERM; Y:TERM):SUB;
	ENTRY ISVAR(X) ∧ ¬OCCUR(X,Y);
	EXIT  MGUT(X,Y,PAIR) ∧ MGUT(Y,X,PAIR);
	EXTERNAL;

PROCEDURE SCOMPP(VAR S1:SUB; S2:SUB);
	INITIAL S1=S0;
	EXIT S1=SCOMP(S0,S2);
	EXTERNAL;

FUNCTION OCCUR(X:TERM; Y:TERM):BOOLEAN;	EXIT TRUE;	EXTERNAL;
% CHECK WHETHER VARIABLE X.VT OCCURS IN Y %


PROCEDURE UNIFY(X,Y:TERMLIST; VAR S:SUB);
VAR X1,Y1: TERMLIST;
    X2,Y2: TERM;
    S2: SUB;

BEGIN 

% Initialization of variables %
S:=ZEROSUB;
X1:=X;
Y1:=Y;

WHILE X1.SL AND Y1.SL AND NOT(S.FL) DO 
  BEGIN
    TSUBSTP(X1.HD,S,X2);
    TSUBSTP(Y1.HD,S,Y2);

    IF X2.ST THEN IF Y2.ST
		       THEN BEGIN IF (X2≠Y2) THEN SCOMPP(S,PAIR(X2,Y2));
					% If X2=Y2 nothing need be done %
			    END
		       ELSE IF OCCUR(X2,Y2) THEN S.FL:=TRUE
			     ELSE SCOMPP(S,PAIR(X2,Y2))
     ELSE
    IF Y2.ST THEN IF OCCUR(Y2,X2) THEN S.FL:=TRUE
		       ELSE SCOMPP(S,PAIR(Y2,X2))
     ELSE
    IF X2.FNLT=Y2.FNLT THEN BEGIN UNIFY(X2.ARGS↑, Y2.ARGS↑, S2);
				  IF S2.FL THEN S.FL:=TRUE
				     % S2 is not a unifier, but indicates failure %
				   ELSE SCOMPP(S,S2)
			      END
     ELSE S.FL:=TRUE;

    X1:=X1.TL↑;
    Y1:=Y1.TL↑;
  END; % End of WHILE body %

IF X1.SL OR Y1.SL  THEN S.FL:=TRUE;

END; % Procedure body %

∂08-May-79  1224	FWH  
 ∂06-May-79  0946	RED  	pascal   
believe it or not i think i have a unifier that will work. At least it
compiles, I haven't yet gotten the courage up to run it on anything.
My immediate problem is how to accomplish a standardize-apart in
pascal.  I think I need the equivalent of GENSYM but I can't think of
any straightforward way to write one in pascal....any ideas?
					ruth
--- If you are using records and pointers (as you probably have to in Pascal
anyway) then the NEW should give you a new pointer. However, if all you need
is just atoms than you have to implement a gensym yourself. After all, Pascal
is not the language to simulate Lisp in; it does not give you ANYTHING for
free.... By the way, how much differs your unifier from our old program ?
Wanna get it "verified"?		Friedrich